\begin{tabbing}
w\_locle($w$;$x$;$y$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$x$ \+
\\[0ex]rel\_star(w{-}E($w$);($\lambda$$x$,$y$. $\neg$first($\lambda$$e$.w{-}pred($w$;$e$);$y$)
\\[0ex]\& $x$ $=$ pred($\lambda$$e$.w{-}pred($w$;$e$);$y$) $\in$ w{-}E($w$))) $y$
\-
\end{tabbing}